(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 57))
(declare-fun v1 () (_ BitVec 85))
(declare-fun a2 () (Array  (_ BitVec 106)  (_ BitVec 100)))
(declare-fun a3 () (Array  (_ BitVec 14)  (_ BitVec 42)))
(assert (let ((e4(_ bv1913452792752847050462213041 91)))
(let ((e5 (bvsub ((_ zero_extend 28) v0) v1)))
(let ((e6 (bvneg e4)))
(let ((e7 (store a3 ((_ extract 52 39) e4) ((_ extract 45 4) e6))))
(let ((e8 (store a3 ((_ extract 50 37) v0) ((_ extract 61 20) v1))))
(let ((e9 (select e7 ((_ extract 19 6) v0))))
(let ((e10 (store a2 ((_ sign_extend 15) e4) ((_ zero_extend 15) e5))))
(let ((e11 (bvmul e5 ((_ zero_extend 43) e9))))
(let ((e12 ((_ rotate_left 58) e6)))
(let ((e13 (bvadd ((_ sign_extend 49) e9) e6)))
(let ((e14 (bvnor e11 e5)))
(let ((e15 (ite (bvugt v1 v1) (_ bv1 1) (_ bv0 1))))
(let ((e16 (ite (distinct v0 v0) (_ bv1 1) (_ bv0 1))))
(let ((e17 (ite (bvuge e5 e11) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvand e14 ((_ zero_extend 84) e16))))
(let ((e19 (bvnand e4 ((_ zero_extend 34) v0))))
(let ((e20 (bvsge e14 ((_ sign_extend 28) v0))))
(let ((e21 (bvslt e12 ((_ sign_extend 6) e5))))
(let ((e22 (bvuge e14 e14)))
(let ((e23 (bvsge ((_ zero_extend 90) e15) e19)))
(let ((e24 (bvule e13 ((_ zero_extend 90) e16))))
(let ((e25 (distinct e6 e13)))
(let ((e26 (distinct ((_ zero_extend 84) e17) e18)))
(let ((e27 (bvugt v1 v1)))
(let ((e28 (bvule e12 e13)))
(let ((e29 (distinct ((_ sign_extend 90) e16) e19)))
(let ((e30 (bvsle e19 e13)))
(let ((e31 (bvsge e18 ((_ zero_extend 84) e17))))
(let ((e32 (bvsgt e17 e17)))
(let ((e33 (distinct e11 ((_ zero_extend 84) e17))))
(let ((e34 (bvule v0 ((_ zero_extend 15) e9))))
(let ((e35 (= e12 ((_ sign_extend 6) e11))))
(let ((e36 (bvule e6 ((_ sign_extend 6) e14))))
(let ((e37 (bvslt e14 ((_ zero_extend 28) v0))))
(let ((e38 (bvuge e12 e13)))
(let ((e39 (bvsge e13 e19)))
(let ((e40 (bvuge e19 e6)))
(let ((e41 (bvsge e19 e12)))
(let ((e42 (bvugt e19 ((_ sign_extend 90) e15))))
(let ((e43 (bvugt e6 e19)))
(let ((e44 (distinct e12 ((_ sign_extend 90) e17))))
(let ((e45 (bvsgt e14 ((_ sign_extend 43) e9))))
(let ((e46 (bvsgt e4 ((_ zero_extend 34) v0))))
(let ((e47 (ite e35 e22 e45)))
(let ((e48 (= e32 e47)))
(let ((e49 (xor e25 e31)))
(let ((e50 (and e39 e48)))
(let ((e51 (or e40 e36)))
(let ((e52 (and e42 e30)))
(let ((e53 (xor e29 e49)))
(let ((e54 (or e21 e26)))
(let ((e55 (and e43 e54)))
(let ((e56 (and e55 e27)))
(let ((e57 (xor e37 e44)))
(let ((e58 (not e57)))
(let ((e59 (=> e24 e52)))
(let ((e60 (not e50)))
(let ((e61 (or e53 e53)))
(let ((e62 (and e51 e56)))
(let ((e63 (=> e34 e23)))
(let ((e64 (or e61 e28)))
(let ((e65 (ite e41 e33 e60)))
(let ((e66 (=> e20 e62)))
(let ((e67 (= e65 e46)))
(let ((e68 (xor e63 e63)))
(let ((e69 (not e38)))
(let ((e70 (ite e69 e67 e69)))
(let ((e71 (ite e58 e66 e64)))
(let ((e72 (=> e70 e70)))
(let ((e73 (xor e71 e68)))
(let ((e74 (= e72 e72)))
(let ((e75 (xor e74 e74)))
(let ((e76 (and e75 e73)))
(let ((e77 (and e59 e76)))
e77
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
